/*
 * Heap.cuh
 *
 *  Created on: Dec 6, 2013
 *      Author: jaime
 */

#ifndef HEAP_CUH_
#define HEAP_CUH_

#include "../SATSolver/SolverTypes.cuh"

struct weighed_literal
{
	Lit literal;
	int weight;
	bool free;
	__device__ void print() { print_lit(literal);
	printf(" (%d),%s ", weight, free ? "f" : "l"); }
};

class var_indexed_vector
{
private:
	unsigned int* indices;
	weighed_literal* vector;
	int number_of_variables;
	int size;


public:
	__device__ var_indexed_vector(int number_of_variables);
	__device__ int get_size();
	__device__ weighed_literal get_weighed_literal(Lit literal);
	__device__ int get_index(Lit literal);
	__device__ weighed_literal get_weighed_literal(int index);
	__device__ void swap(unsigned int index_1, unsigned int index_2);
	__device__ void increment(int index, int increment);
	__device__ bool is_free(Lit literal);
	__device__ void set_free(Lit literal, bool free);
	//Test method
	__device__ void print();
};

class Heap {
private:
	var_indexed_vector vector;
	bool* variables_free_status;
	__device__ int parent_index(int index);
	__device__ int left_child_index(int index);
	__device__ int right_child_index(int index);
public:
	__device__ Heap(int number_of_variables);
	__device__ Lit get_max_lit();
	__device__ void increment_lit(Lit literal, int increment);
	__device__ bool is_free(Var variable);
	__device__ void set_free(Var variable, bool free);

	//Test method
	__device__ void print();

};

#endif /* HEAP_CUH_ */
